Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,from(s(X)))
2:		2ndspos(0,Z)	→ rnil
3:		2ndspos(s(N),cons(X,Z))	→ 2ndspos(s(N),cons2(X,Z))
4:		2ndspos(s(N),cons2(X,cons(Y,Z)))	→ rcons(posrecip(Y),2ndsneg(N,Z))
5:		2ndsneg(0,Z)	→ rnil
6:		2ndsneg(s(N),cons(X,Z))	→ 2ndsneg(s(N),cons2(X,Z))
7:		2ndsneg(s(N),cons2(X,cons(Y,Z)))	→ rcons(negrecip(Y),2ndspos(N,Z))
8:		pi(X)	→ 2ndspos(X,from(0))
9:		plus(0,Y)	→ Y
10:		plus(s(X),Y)	→ s(plus(X,Y))
11:		times(0,Y)	→ 0
12:		times(s(X),Y)	→ plus(Y,times(X,Y))
13:		square(X)	→ times(X,X)

There are 11 dependency pairs:


14:		FROM(X)	→ FROM(s(X))
15:		2ndspos#(s(N),cons(X,Z))	→ 2ndspos#(s(N),cons2(X,Z))
16:		2ndspos#(s(N),cons2(X,cons(Y,Z)))	→ 2ndsneg#(N,Z)
17:		2ndsneg#(s(N),cons(X,Z))	→ 2ndsneg#(s(N),cons2(X,Z))
18:		2ndsneg#(s(N),cons2(X,cons(Y,Z)))	→ 2ndspos#(N,Z)
19:		PI(X)	→ 2ndspos#(X,from(0))
20:		PI(X)	→ FROM(0)
21:		PLUS(s(X),Y)	→ PLUS(X,Y)
22:		TIMES(s(X),Y)	→ PLUS(Y,times(X,Y))
23:		TIMES(s(X),Y)	→ TIMES(X,Y)
24:		SQUARE(X)	→ TIMES(X,X)

The approximated dependency graph contains 4 SCCs: {15-18}, {14}, {21} and {23}.

Consider the SCC {15-18}. There are no usable rules. By taking the AF π with π(2ndsneg#) = π(2ndspos#) = 1 together with the lexicographic path order with empty precedence, the rules in {15,17} are weakly decreasing and the rules in {16,18} are strictly decreasing.

Consider the SCC {14}. There are no usable rules. The constraints could not be solved.

Consider the SCC {21}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.

Consider the SCC {23}. There are no usable rules. By taking the AF π with π(TIMES) = 1 together with the lexicographic path order with empty precedence, rule 23 is strictly decreasing.

Tyrolean Termination Tool (0.25 seconds) --- May 4, 2006